\begin{tabbing}
$\forall$${\it the\_w}$:World.
\\[0ex]FairFifo
\\[0ex]$\Rightarrow$ \=val{-}axiom(E;${\it the\_w}$.TA;${\it the\_w}$.M;$\lambda$$e$.w{-}info(${\it the\_w}$;$e$);$\lambda$$e$.w{-}pred(${\it the\_w}$;$e$);\+
\\[0ex]$\lambda$$i$,$x$. s($i$;0).$x$;$\lambda$$i$.(w{-}machine(${\it the\_w}$;$i$).2).1;
\\[0ex]$\lambda$$i$.w{-}machine(${\it the\_w}$;$i$).1;$\lambda$$i$.w{-}machine(${\it the\_w}$;$i$).2.2;$\lambda$$e$.val($e$);$\lambda$$e$.time($e$))
\-
\end{tabbing}